Inference at * 1 1 
Iof proof for Lemma complete nat ind with y:

.....subterm..... T:t1:n

1. P : {k}
2. g : i:. (j:i. P(j))  P(i)
  Y(f,x. g(x,f))  (i:. P(i)) 

latex

 by Assert Y(f,x. g(x,f))  VoidVoid 

latex

 1: .....assertion..... NILNIL

 1:   Y(f,x. g(x,f))  VoidVoid
 2: 

 2: 3. Y(f,x. g(x,f))  VoidVoid
 2:   Y(f,x. g(x,f))  (i:. P(i))
 .

Definitions

t  T, x:AB(x), Void, Y, x.A(x), f(a)